import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import sign.FormulaSign;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Random;
import java.util.Set;

public class GF {
    //10个ua（5+5），6个ba（3+3）
    public ArrayList<UnaryFormula> getUAs(){//get unary atoms
        // 创建 uaPremise1 数组，包含 p1 到 p5
        String[] uaPremise = new String[5];
        for (int i = 0; i < uaPremise.length; i++) {
            uaPremise[i] = "p" + (i + 1);
        }

        ArrayList<UnaryFormula> ufArr=new ArrayList<>();
        for (String ua:uaPremise) {
            UnaryFormula uf=new UnaryFormula(new UnaryLiteral(new UnaryAtom(ua),false));//生成（p1-p5）正的uf
            ufArr.add(uf);
        }

        for (String ua:uaPremise) {
            UnaryFormula uf=new UnaryFormula(new UnaryLiteral(new UnaryAtom(ua),true));//生成（p1-p5）负的uf
            ufArr.add(uf);
        }

        return ufArr;
    }

    public ArrayList<UnaryFormula> getBAs(){//get binary atoms
        // 创建 baPremise 数组，包含 r1 到 r3
        String[] baPremise = new String[3];
        for (int i = 0; i < baPremise.length; i++) {
            baPremise[i] = "r" + (i + 1);
        }

        ArrayList<UnaryFormula> baArr=new ArrayList<>();//binary atom也是以uf的形式存在
        for (String ba:baPremise) {
            UnaryFormula uf=new UnaryFormula(new UnaryLiteral(new UnaryAtom(ba),false));//生成（r1-r3）正的uf
            baArr.add(uf);
        }

        for (String ba:baPremise) {
            UnaryFormula uf=new UnaryFormula(new UnaryLiteral(new UnaryAtom(ba),true));//生成（r1-r3）负的uf
            baArr.add(uf);
        }

        return baArr;
    }

    public ArrayList<UnaryFormula> selectUAs(int x,ArrayList<UnaryFormula> uaArr){
        x=x/10;
        Set<UnaryFormula> resultSet = new HashSet<>();
        Random rand = new Random();

        while (resultSet.size() < x) {
            int index = rand.nextInt(uaArr.size());
            resultSet.add(uaArr.get(index));  // HashSet 自动去重
        }

        ArrayList<UnaryFormula> selected = new ArrayList<>(resultSet);

        return selected;
    }

    public ArrayList<UnaryFormula> selectBAs(int y,ArrayList<UnaryFormula> baArr){
        //从baArr中选择（y/10）个不重复的ba，以arraylist形式返回
        y=y/10;
        Set<UnaryFormula> resultSet = new HashSet<>();
        Random rand = new Random();

        while (resultSet.size() < y) {
            int index = rand.nextInt(baArr.size());
            resultSet.add(baArr.get(index));  // HashSet 自动去重
        }

        ArrayList<UnaryFormula> selected = new ArrayList<>(resultSet);

        return selected;
    }

    public BinaryFormula generateBF(ArrayList<UnaryFormula> selectedUA){
        //selectedUA:包含（x/10）个ua
        Random random=new Random();
        int number1= random.nextInt(selectedUA.size());
        int number2=random.nextInt(selectedUA.size());//从selectedUA中的ua中选取组成bf
        int sign=random.nextInt(2);//random sign

        if (sign==0){//exist
            BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,selectedUA.get(number1), selectedUA.get(number2));
            return bf;
        }else{//any
            BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,selectedUA.get(number1), selectedUA.get(number2));
            return bf;
        }
    }

    public BinaryFormula generateTF(ArrayList<UnaryFormula> selectedUA,ArrayList<UnaryFormula> selectedBA){
        //selectedUA:包含（x/10）个ua
        //selectedBA:包含（y/10）个ba
        Random random=new Random();
        int sign1=random.nextInt(2);//random sign
        int sign2=random.nextInt(2);//random sign(inner one)
        int number1= random.nextInt(selectedUA.size());
        int number2=random.nextInt(selectedUA.size());//从selectedUA（x/10 个ua）中选择
        int number3=random.nextInt(selectedBA.size());//从selectedBA（y/10 个ba）中选择

        if (sign1==0){//outer sign is exist
            if (sign2==0){//inner sign is exist
                //total formula is (E,E)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST, selectedUA.get(number2),selectedBA.get(number3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST, selectedUA.get(number1), bfInner);
                return bf;
            }else{//inner sign is for any
                //total formula is (E,A)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,selectedUA.get(number2),selectedBA.get(number3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,selectedUA.get(number1), bfInner);
                return bf;
            }
        }else {//outer sign is for all
            if (sign2==0){//inner sign is exist
                //total formula is (A,E)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,selectedUA.get(number2),selectedBA.get(number3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY, selectedUA.get(number1), bfInner);
                return bf;
            }else{//inner sign is for any
                //total formula is (A,A)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,selectedUA.get(number2),selectedBA.get(number3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY, selectedUA.get(number1), bfInner);
                return bf;
            }
        }
    }

    public BinaryFormula generateConclusion(ArrayList<UnaryFormula> selectedUA,ArrayList<UnaryFormula> selectedBA){
        Random random=new Random();
        int flag= random.nextInt(2);
        if (flag==0){//生成bf
            return generateBF(selectedUA);
        }else {//生成tf
            return generateTF(selectedUA,selectedBA);
        }
    }

    public ArrayList<BinaryFormula> getConditions(ArrayList<UnaryFormula> selectedUA,ArrayList<UnaryFormula> selectedBA){
        //生成10个formulas，bf和tf数量随机
        Random random=new Random();
        int bfN=random.nextInt(11);//number of BF,0到10
        int tfN=10-bfN;
//        System.out.println("bfN = "+bfN);
//        System.out.println("tfN = "+tfN);

        ArrayList<BinaryFormula> conditions=new ArrayList<>();
        for (int i = 0; i < bfN; i++) {//生成bfN个bf
            conditions.add(generateBF(selectedUA));
        }
        for (int i = 0; i < tfN; i++) {//生成tfN个tf
            conditions.add(generateTF(selectedUA,selectedBA));
        }

        return conditions;
    }

    public Proof run(ArrayList<UnaryFormula> selectedUA,ArrayList<UnaryFormula> selectedBA,BinaryFormula conclusion){
        ArrayList<BinaryFormula> conditions=getConditions(selectedUA,selectedBA);
        ArrayList<Proof> proofs=new ArrayList<>();
        for (BinaryFormula condition:conditions) {
            proofs.add(new ConclusionProof(condition));
        }
//        System.out.println(proofs);
//        System.out.println(conclusion);
//        System.out.println("-------------------");

        //System.out.println(Solve.solveHelper(proofs,conclusion, new UsedCondition()));
        Proof result=Solve.solveHelper(proofs,conclusion, new UsedCondition());
        return result;


    }

    public static void main(String[] args) {
        GF gf = new GF();
        ArrayList<UnaryFormula> ufArr = gf.getUAs();
        ArrayList<UnaryFormula> baArr= gf.getBAs();//固定数值，不参与循环
        //float count=0;

// 外层循环遍历x值（10到100，步长10）
        int start_x = 10;
        int start_y = 10;
        int end_x = 100;
        int end_y = 60;
        int step = 10;

        for (int x = start_x; x <= end_x; x += step) {
            // 内层循环遍历y值（10到60）
            for (int y = start_y; y <= end_y; y += step) {
                int count = 0; // 每个(x,y)组合的计数重置

                // 原来的100次实验循环
                for (int i = 0; i < 100; i++) {
                    ArrayList<UnaryFormula> selectedUA = gf.selectUAs(x, ufArr);
                    ArrayList<UnaryFormula> selectedBA = gf.selectBAs(y, baArr);
                    BinaryFormula conclusion = gf.generateConclusion(selectedUA, selectedBA);

                    Proof result = gf.run(selectedUA, selectedBA, conclusion);
                    if (result != null) {
                        count = count + 1;
//                        System.out.println(result);
//                        System.out.println(" ");
                    } else {
//                        System.out.println("null");
//                        System.out.println(" ");
                    }
                }

                // 输出当前(x,y)组合的结果
                System.out.println("x=" + x + ", y=" + y + " done");
                System.out.println(count);
                float probability = (count / 100.0f) * 100; // 注意使用100.0f避免整数除法
                String formatted = String.format("%.2f", probability);
                System.out.println("P=" + formatted + "%");
                System.out.println("----------------------"); // 分隔不同组合的结果
            }
        }







//        System.out.println("For UA:");
//        for (UnaryFormula uf:selectedUA) {
//            System.out.println(uf);
//        }
//        System.out.println("For BA:");
//        for (UnaryFormula uf:selectedBA) {
//            System.out.println(uf);
//        }
//        for (int i = 0; i < 10; i++) {
//            System.out.println(gf.generateBF(selectedUA));
//        }
//
//        System.out.println("");
//
//        for (int i = 0; i < 10; i++) {
//            System.out.println(gf.generateTF(selectedUA,selectedBA));
//        }
//        ArrayList<BinaryFormula> conditions=gf.getConditions(selectedUA,selectedBA);
//        for (BinaryFormula bf:conditions) {
//            System.out.println(bf);
//        }



    }
}
